g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))
↳ QTRS
↳ DependencyPairsProof
g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))
F(0, 1, x) → F(s(x), x, x)
F(x, y, s(z)) → F(0, 1, z)
g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F(0, 1, x) → F(s(x), x, x)
F(x, y, s(z)) → F(0, 1, z)
g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(x, y, s(z)) → F(0, 1, z)
Used ordering: Polynomial interpretation [25,35]:
F(0, 1, x) → F(s(x), x, x)
The value of delta used in the strict ordering is 1/16.
POL(s(x1)) = 1/4 + x_1
POL(F(x1, x2, x3)) = (1/4)x_3
POL(0) = 15/4
POL(1) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
F(0, 1, x) → F(s(x), x, x)
g(x, y) → x
g(x, y) → y
f(0, 1, x) → f(s(x), x, x)
f(x, y, s(z)) → s(f(0, 1, z))